R:Realizer, names:(MaName List). R|names  Realizer 

latex

Definitions	R|names, t  T, x:A. B(x)
Lemmas	MaName wf, R-names wf, Rnone wf, es realizer wf, manames-overlap-case wf, Rtransform wf